e copies x
== a:Atom1.
== (loc(e) >> a  x when es-init(es;e):vartype(loc(e);x)>>a)
== & state when e\\x:state@loc(e)\\x>>a
== & e receives a
== & state after e\\x:state@loc(e)\\x>>a 

latex

---

clarification:

es-copies(es;e;x)
== a:Atom1.
== (es-atom(es;es-loc(es; e);a)
== ( es-when(es; x; es-init(es;e)):es-vartype(es; es-loc(es; e); x)>>a)
== & es-state-when-without(es;e;x):es-state-without(es;es-loc(es; e);x)>>a
== & es-rcv-atom(es;e;a)
== & es-state-after-without(es;e;x):es-state-without(es;es-loc(es; e);x)>>a 

latex

Definitions	x:A. B(x), Atom$n, P  Q, vartype(i;x), x when e, es-init(es;e), state when e\\x, P & Q, A, e receives a, x:T>>a, state@i\\x, loc(e), state after e\\x
FDL editor aliases	es-copies